COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	More applications of circumscription
C00007 ENDMK
C⊗;
More applications of circumscription

1. frame problem

2. ∃x.P(x) → ∃x.∀y.(P(y) ≡ y=x)

3. P(a) ∨ P(b) → ∃x.(x=a ∨ x=b ∧ ∀y.(P(y) ≡ y = x))

4. ∃x.R(x)∧P(x) → ∃x.(R(x) ∧ ∀y.(P(y) ≡ y = x))

5. Pressure depends only on volume and temperature.


***

When is a circumscription replacable by a single formula?
If when the formula is put in clausal form, no two clauses
allow rubbing literals involving P against each other.
Does the resolution way of writing formulas simplify circumscription
or proving things about it?  At first glance, no.

***
	A new kind of circumscription seems to be required or at least
useful in order to do the frame problem properly.  Thus we would like
to say that when something moves, everything that could stay where it
was does so.  We do it as follows:

We have

	∀y z s.(loc(y,move(y,z,s)) = z)

We want to prescribe the function  loc(x,s)  so as to minimize the
expression

	loc(x,s) ≠ loc(x,move(y,z,s)),

and we can express this by the schema

	∀y z s.(phi(y,move(y,z,s)) = z) 

⊃ ∀x y z s.(phi(x,move(y,z,s)) = phi(x,s) ⊃ loc(move(y,z,s) = loc(x,s))).

We might also say

	∀y z s.(phi(y,move(y,z,s)) = z) 

⊃ ∀x y z s.(phi(x,move(y,z,s)) = loc(x,s) ⊃ loc(move(y,z,s) = loc(x,s))).



	Suppose we have blocks A and B and Table and

	loc(A,s0) = Table ∧ loc(B,s0) = Table ∧ loc(Table,s0) = Table.

Then we write

	phi(A,s0) = Table ∧ 

**** More new circumscription

∀y z s.(loc(y,move(y,z,s)) = z)

expresses the intended result of moving y to z.  Determining loc so
as to minimize the truth of

loc(x,move(y,z,s)) ≠ loc(x,s)

results in the schema

∀y z s.(f(y,move(y,z,s) =z) 
	∧ ∀x y z s.(¬(f(x,move(y,z,s)) = f(x,s)) ⊃ ¬(loc(x,move(y,z,s))=loc(x,s)))
	⊃ ∀x y z s.(¬(loc(x,move(y,z,s)) = loc(x,s)) ⊃ ¬(f(x,move(y,z,s))=f(x,s))))

	Alternatively, we can use the relation on(x,y,s) starting with

∀y z s.on(y,z,move(y,z,s))

which should circumscribe to

∀y z s.P(y,z,move(y,z,s)) 
∧ ∀w x y z s.(¬(P(x,w,move(y,z,s))≡P(x,w,s)) ⊃ ¬(on(x,w,move(y,z,s))≡on(x,w,s)))
⊃ ∀w x y z s.(¬(on(x,w,move(y,z,s))≡on(x,w,s)) ⊃ ¬(P(x,w,move(y,z,s))≡P(x,w,s))).

These can be expressed more simply as

	loc(y,move(y,z,s)) = z

and we let phi(x) correspond to loc(x,move(y,z,s) giving the generalized
circumscription

	phi(y) = z ∧ ∀x.(phi(x) ≠ loc(x,s) ⊃ loc(x,move(y,z,s)) ≠ loc(x,s))
		 ⊃ ∀x.(loc(x,move(y,z,s)) ≠ loc(x,s) ⊃ phi(x) ≠ loc(x,s)).

Setting

	phi(x) = if x=y then z else loc(x,s)

yields eventually

	∀x.(x ≠ y ⊃ loc(x,move(y,z,s)) = loc(x,s)).

This is what is wanted, and if the statement  loc(y,move(y,z,s))  were
elaborated, for example by asserting that objects attached to  y  remain
don't change location, the circumscription would give the appropriate
results.

	The new terminology might be minimizing the wff

	loc(x,move(y,z,s)) ≠ loc(x,s)

with respect to the argument λx.loc(x,move(y,z,s) while holding constant
the statement

	loc(y,move(y,z,s)) = z.